/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.type;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Iterator;
import java.util.List;

import alloy.ast.Expr;
import alloy.util.Dbg;

/**
 * represents a relation type, a non-empty sequence of
 * {@link BasicType}s.  All expressions in a semantically
 * correct Alloy model have a RelationType associated with
 * them.  RelationTypes are immutable.
 * NOTE:  RelationTypes must implement Comparable in order for
 * the backend (sharing detection) to work!
 */

public class RelationType implements Comparable {

    /**
     * holds sequence of {@link BasicType}s
     */
    private List _basicTypes;

    /** cached copy of string */
    private String _typeString;

    private RelationType(int arity) {
        Dbg.check(arity > 0);
        _basicTypes = new ArrayList(arity);
    }

    /**
     * Creates a new RelationType that is equal to rt_
     * @param rt_ relation type
     **/
    private RelationType(RelationType rt_) {
        this(rt_.arity());
        _basicTypes.addAll(rt_._basicTypes);
    }

    /**
     * Constructs a RelationType that is a sequence of BasicTypes specified by the given List
     * @param basicTypes_ a List of BasicTypes that will comprise this.  It is required that
     * members of basicTypes_ either all be EmptyType or all not be instances of EmptyType
     * @throws IllegalArgumentException if members of basicTypes_ are not either all EmptyType or
     * all not be instances of EmptyType
     **/
    public RelationType(List basicTypes_) {
    this(basicTypes_.size());
    Iterator iter = basicTypes_.iterator();
    BasicType bt = (BasicType) iter.next();
    boolean empty = bt.isEmpty();
    _basicTypes.add(bt);
    while (iter.hasNext()) {
        bt = (BasicType) iter.next();
        if (empty != bt.isEmpty())
        throw new IllegalArgumentException();
        _basicTypes.add(bt);
    }
    }
    /**
     * @param firstType_ the first basic type of this
     */
    public RelationType(BasicType firstType_) {
        this(1);
        Dbg.check(firstType_ != null, "null first type");
        _basicTypes.add(firstType_);	
    }

    /**
     * Returns true if this is an empty product; that is, a product of the form EmptyType->EmptyType->...;
     * otherwise returns false
     * @return true if this is an empty product; that is, a product of the form EmptyType->EmptyType->...;
     * otherwise returns false
     **/
    public boolean isEmpty() {
    // note that we only need to look at the first BasicType in the sequence
    // since the we don't allow sequences that mix EmptyType with other BasicTypes
    return getBasicTypeAt(0).isEmpty();
    }

    /**
     * Tests if every BasicTypes in this is a subtype of the corresponding BasicType
     * in rt_.  For instance, if A1 is a subtype of A, then A1->B is a subtype of A->B.
     * @param rt_ an instance of RelationType which has the same arity as this
     * @return true if <code>this</code> is a subset of rt_; otherwise raturns false.
     **/
    public boolean isSubsetOf(RelationType rt_) {
    if (arity() != rt_.arity()) return false;

    Iterator iter1 = this.getTypeIter();
    Iterator iter2 = rt_.getTypeIter();

    while (iter1.hasNext()) {

        BasicType bt1 = (BasicType) iter1.next();
        BasicType bt2 = (BasicType) iter2.next();

        if (!bt1.isSubtypeOf(bt2)) return false;

    }

    return true;
    }

    /**
     * Computes the intersection of two RelationTypes, if any.  rt_ must
     * have the same arity as this.
     * @param rt1_ RelationType
     * @return return a new RelationType rt' such that for each 0<=i<rt'.arity(), q
     * rt'(i) = this(i).intersect(rt_(i)) iff !this(i).intersect(rt_(i)).isEmpty() for
     * all i.  If this(i).intersect(rt_(i)).isEmpty() for some i, then rt'(i) = EmptyType.EMPTY_TYPE
     * for all i.
     * @throws InvalidAritiesException if this.arity() != rt_.arity()
     **/
    public RelationType intersect(RelationType rt_) throws InvalidAritiesException {

    if (this.arity() != rt_.arity())
        throw new InvalidAritiesException();

    RelationType ret;

    Iterator iter1 = this.getTypeIter();
    Iterator iter2 = rt_.getTypeIter();

    ret = new RelationType(arity());

    while (iter1.hasNext()) {
        BasicType bt1 = (BasicType) iter1.next();
        BasicType bt2 = (BasicType) iter2.next();
        BasicType result = bt1.intersect(bt2);
        // if the intersection of two BasicTypes is empty, then the types don't intersect
        if (result.isEmpty()) {
        //ret._basicTypes = Collections.nCopies(arity(), EmptyType.EMPTY_ERROR_TYPE);
        ret._basicTypes = Collections.nCopies(arity(), EmptyType.EMPTY_TYPE);
        break;
        } else {
        ret._basicTypes.add(result);
        }
    }

    return ret;
    }

    public static RelationType join(RelationType rt1_, RelationType rt2_) { return rt1_.join(rt2_); }
									   

    /**
     * Joins this and rt_, if possible
     * @param rt_ RelationType to join to this
     * @return a new RelationType rt' such that rt' = this.rt_.  rt' is null
     * if this and rt_ cannot be joined.  The requirement for a successful join
     * is that this.arity() + rt_.arity() >= 3 and the rightmost
     * BasicType of this and the leftmost BasicType of rt_ intersect.
     * @throws InvalidAritiesException is thrown if the sum of arities of this and rt_ is less than 3.
     * @throws InvalidJoinException if the intersection of rightmost BasicType of this and the leftmost
     * BasicType of rt_ is EmptyType.
     **/
    public RelationType join(RelationType rt_) throws InvalidAritiesException, InvalidJoinException {

        int leftSize = arity();
        int rightSize = rt_.arity();

        if (leftSize + rightSize < 3)
            throw new InvalidAritiesException();

        // if the intersection of BasicTypes results in an EmptyType, then the types don't intersect
        if (getBasicTypeAt(leftSize - 1).intersect(rt_.getBasicTypeAt(0)).isEmpty())
            throw new InvalidJoinException();


        RelationType retType = new RelationType(leftSize+rightSize-2);

        if (leftSize > 1)
            retType._basicTypes.addAll(_basicTypes.subList(0, leftSize - 1));

        if (rightSize > 1)
            retType._basicTypes.addAll(rt_._basicTypes.subList(1, rightSize));

        if (retType.arity() < 1) {
            //System.out.println("join " + this + " and " + rt_);
            throw new RuntimeException();
        }

        return retType;
    }

    public int numBasicTypes() {
        return arity();
    }

    /**
     * Creates a new RelationType with the basic types of the given relation
     * type appended to the basic types of this.
     * @param other_ the appended RelationType; other_.isEmpty() must return
     * the same value as this.isEmpty()
     * @return the new RelationType b1->...->bn such that this = b1->...->bi and
     * other_ = b(i+1)->...->bn
     * @throws IllegalArgumentException if other_.isEmpty() XOR this.isEmpty()
     * is true.
     */
    public RelationType product(RelationType other_) {
    if (this.isEmpty() != other_.isEmpty())
        throw new IllegalArgumentException();

    RelationType retType = new RelationType(arity()+other_.arity());
    retType._basicTypes.addAll(this._basicTypes);
    retType._basicTypes.addAll(other_._basicTypes);
    return retType;
    }

    public static RelationType product(RelationType r1_, RelationType r2_) { return r1_.product(r2_); }

    /**
     * Creates a new RelationType whose BasicTypes are in the reverse
     * order of the BasicTypes of this.
     * @return a new RelationType that is a transpose of this
     **/
    public RelationType transpose() {
    RelationType ret = new RelationType(this);
    Collections.reverse(ret._basicTypes);
    return ret;
    }

    /**
     * @return If this[column] & bt is non-empty, then returns a new RelationType
     * rt = this[0]->this[1]->...this[column]&bt->...->this[this.arity()].  Otherwise
     * returns an empty RelationType of the same arity as this
     **/
    public RelationType columnRestrict(BasicType bt, int column) {
    BasicType btColumn = this.getBasicTypeAt(column);
    BasicType btIntersect = bt.intersect(btColumn);
    List bTypes;

    if (btIntersect.isEmpty()) {
        bTypes = Collections.nCopies(this.arity(), EmptyType.EMPTY_TYPE);
    } else {
        bTypes = new ArrayList(this._basicTypes);
        bTypes.set(column, btIntersect);
    }

    return new RelationType(bTypes);

    }

    /**
     * get the number of basic types in this
     * @return the number of basic types
     */
    public int arity() {
        return _basicTypes.size();
    }

    /**
     * get an Iterator of the basic types of this
     * @return the Iterator
     */
    public Iterator getTypeIter() {
        return _basicTypes.iterator();
    }

    /**
       @return a list of {@link String}s corresponding
       to the basic types of this, in order
    */
    public ArrayList getTypeNameArrayList() {
    ArrayList typeNames = new ArrayList();
    for(int i =0; i< _basicTypes.size(); i++){
        typeNames.add(((BasicType)_basicTypes.get(i)).toString());
    }
        return typeNames;
    }


    /**
     * Return a newly allocated array of scopes
     * of the basic types of this, in order.  Can be given to
     * {@link alloy.util.MultiDimIter} to iterate over
     * indices of tuples for this {@link RelationType} for the
     * current analysis scopes set for the {@link BasicType}s.
     * The returned array must not be modified.
     */
    public int[] getScopes() {
    int[] scopes = new int[arity()];
    for (int i=0; i< scopes.length; i++)
        scopes[i] = getBasicTypeAt(i).getScope();

    return scopes;
    }

    /**
     * Return the number of tuples in relations of this {@link RelationType}.
     */
    public int getNumTuples() {
    int n = 1;
    for (int i=0; i<arity(); i++)
        n *= getBasicTypeAt(i).getScope();
    return n;
    }

    /** Returns an immutable List view of the BasicTypes of this
     * @return an immutable List view of the BasicTypes of this **/
    public List getBasicTypes() {
    return Collections.unmodifiableList(_basicTypes);
    }
    /**
     * get the basic type at some index
     * @param index_ the index
     * @return the BasicType
     */
    public BasicType getBasicTypeAt(int index_) {
        Dbg.check(!(index_ < 0 || index_ >= _basicTypes.size()), "index out of bounds");
        return (BasicType)_basicTypes.get(index_);
    }

    /** Test whether this RelationType includes the given {@link BasicType} as one of its columns */
    public boolean includesBasicType(BasicType basicType_) {
    for (int i=0; i<arity(); i++)
        if (getBasicTypeAt(i).equals(basicType_))
        return true;
    return false;
    }

    /** Get the {@link SigType} which is the first {@link BasicType} of
     this.  <em>NOTE:</em> should not be called if first basic type
    of this is not a {@link SigType}. */
    public SigType getSigType() {
        Dbg.check(getBasicTypeAt(0) instanceof SigType);
        return (SigType)getBasicTypeAt(0);
    }

    /** @return the full strings of the basic types of this,
        separated by "-&gt;"
        @see #_toString
     */
    public String toString() {
    if (_typeString == null) {
        _typeString = _toString(false);
    }
    return _typeString;
    }

    /** @return possibly shortened strings of the basic types
        of this, separated by "-&gt;"
        @see #_toString
    */
    public String toShortString() { return _toString(true); }

    /**
     * returns a string representation of this, the names of basic
     * types separated by "-&gt;"
     * @param canShorten_ if <code>true</code>, tries to shorten
     * the names of the basic types
     * @see BasicType#toShortString
     */
    private String _toString(boolean canShorten_) {
        StringBuffer retString = new StringBuffer();
        Iterator typeIter = getTypeIter();
        while (typeIter.hasNext()) {
            BasicType curType = (BasicType)typeIter.next();
            retString.append(canShorten_ ? curType.toShortString() : curType.toString());
            if (typeIter.hasNext()) {
                retString.append(" -> ");
            }
        }
        return retString.toString();
    }

    /**
     * returns a new expression with this as its type
     */

    public Expr toExpr() {
        Expr retExpr = ((BasicType)_basicTypes.get(0)).toExpr();
        if (_basicTypes.size() > 1) {
            for (int i = 1; i < _basicTypes.size(); i++) {
                Expr curSigExpr = ((BasicType)_basicTypes.get(i)).toExpr();
		retExpr = retExpr.product(curSigExpr);
	    }
        }

        return retExpr;
    }


    /**
     * Check if another object is equal to this.  The object is
     * equal if it is a RelationType with the same basic types as
     * this.
     * @param obj the Object to compare
     * @return <code>true</code> if <code>obj</code> is equal to this; <code>false</code> otherwise
     */
    public boolean equals(Object obj) {
        if (obj instanceof RelationType) {
            RelationType otherType = (RelationType)obj;
            // must have the same number of basic types
            if (otherType.arity() == arity()) {
                for (int i = 0; i < arity(); i++) {
                    // each basic type must be equal by
                    // object equality
                    if (_basicTypes.get(i) != otherType._basicTypes.get(i)) return false;
                }
                return true;
            }
        }

        return false;
    }

    public int hashCode() {
        int ret = 0;
        for (int i = 0; i < _basicTypes.size(); i++) {
            ret += _basicTypes.get(i).hashCode();
        }
        return ret;
    }


    public int compareTo(Object obj_) {
	if (equals(obj_)) return 0;
        RelationType that = (RelationType)obj_;
	// we compare the relationtypes as numbers
	// with basictypes as digits, with the first
	// basictype as the highest-order bit, etc.
	for (int i=0; i<Math.min(arity(), that.arity()); i++) {
	    int c = getBasicTypeAt(i).compareTo(that.getBasicTypeAt(i));
	    if (c != 0) return c;
	}
	return arity() < that.arity() ? -1 : +1;
    }

}
